package typesys;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.TreeSet;

import flowlogic.STSimplifier;

import ast.ActsFor;
import ast.AndPredicate;
import ast.Assert;
import ast.AtomicLabel;
import ast.BasicBinder;
import ast.Binder;
import ast.Call;
import ast.Case;
import ast.ChannelConstant;
import ast.CompositeBinder;
import ast.Dummy;
import ast.ExistsPredicate;
import ast.ForallPredicate;
import ast.Go;
import ast.Label;
import ast.LabelConjunction;
import ast.LabelDisjunction;
import ast.NewConstP;
import ast.NumPredicate;
import ast.OrPredicate;
import ast.ParallelProcess;
import ast.PrefixedProcess;
import ast.Principal;
import ast.Procedure;
import ast.QualityPredicate;
import ast.Site;
import ast.Term;
import ast.Zero;
import ast.Process;

public class ProcessJudgement extends TypeJudgement {
	
	private Process process;
	private HashMap<String, HashSet<Term>> rho;
	private Site site;
	private Label ctxLabel;
	private HashMap<String, Label> gamma;
	private HashMap<String, Procedure> procedureMap;
	
	public ProcessJudgement(Process process,
				   Label ctxLabel,
				   HashMap<String, HashSet<Term>> rho,
				   Site site,
				   HashMap<String, Label> gamma, 
				   PrincipalHierarchy hierarchy)
	{
		this.process = process;
		this.ctxLabel = ctxLabel;
		this.rho = rho;
		this.site = site;
		this.gamma = gamma;
		this.procedureMap = STSimplifier.getProcedureMap();
		setHierarchy(hierarchy);
	}
	
	public boolean check() throws FunctionUndefinedException
	{
		boolean result = false;
		
		if (process instanceof Zero) {
			
			result = true;
			
		} else if (process instanceof Dummy) {
			
			ProcessJudgement pjgt = new ProcessJudgement(
					((Dummy) process).getProcess(), ctxLabel, rho, site, gamma, getHierarchy());
			result = pjgt.check();
			
		} else if (process instanceof Call) {
			
			result = true;

			Procedure callee = procedureMap.get(((Call) process).getName());
			Label beginLabel = callee.getBeginLabel();
			ArrayList<Term> pl = new ArrayList<Term>();
			pl.add(site);
			RelabellingJudgement acjgt = new RelabellingJudgement(
					getHierarchy(),
					new AtomicLabel(TopPrincipal.getInstance(), pl), 
					beginLabel);
			if (!acjgt.check()) {
				result = false;
			} else {
				RelabellingJudgement ctxjgt = new RelabellingJudgement(
						getHierarchy(), ctxLabel,beginLabel);
				if (!ctxjgt.check()) {
					result = false;
				}
			}
			
		} else if (process instanceof ParallelProcess) {
			
			result = true;
			
			for (Process comp : ((ParallelProcess) process).getProcesses()) {
				ProcessJudgement pjdgt = new ProcessJudgement(
						comp, ctxLabel, rho, site, gamma, getHierarchy());
				if (!pjdgt.check()) {
					result = false;
					break;
				}
			}
			
		} else if (process instanceof NewConstP) {
			
			HashMap<String, Label> gammaInner = null;
			if (((NewConstP) process).getConstant() instanceof ChannelConstant) {
				gammaInner = new HashMap<String, Label>();
				gammaInner.putAll(gamma);
				ChannelConstant cst = (ChannelConstant) ((NewConstP) process).getConstant();
				gammaInner.put(cst.getName(), cst.getLabel());
			} else {
				gammaInner = gamma;
			}
			
			ProcessJudgement pjdgt = new ProcessJudgement(
					((NewConstP) process).getProcess(),
					ctxLabel, rho, site, gammaInner, getHierarchy());
			
			result = pjdgt.check();
			
		} else if (process instanceof PrefixedProcess) {
			
			result = true;
			
			Binder bd = ((PrefixedProcess) process).getBinder();
			BinderJudgement bdjdgt = new BinderJudgement(bd, rho, site, gamma, getHierarchy());
			if (!wfif(bd) || !bdjdgt.checkAndDerive()) {
				result = false;
			} else {
				Label innerCtx = bdjdgt.getCtxLabel();
				RelabellingJudgement rejdgt =
						new RelabellingJudgement(getHierarchy(), ctxLabel, innerCtx);
				if (!rejdgt.check()) {
					result = false;
				} else {
					ProcessJudgement pjdgt1 = new ProcessJudgement(
							((PrefixedProcess) process).getProcess(),
							new LabelDisjunction(ctxLabel, bdjdgt.getDerivedLabel()),
							rho, site, gamma, getHierarchy());
					if (!pjdgt1.check())
						result = false;
				}
			}
			
		} else if (process instanceof Case) {
			
			Process p1 = ((Case) process).getProcess1();
			Process p2 = ((Case) process).getProcess2();
			ProcessJudgement pjdgt1 = new ProcessJudgement(
					p1, ctxLabel, rho, site, gamma, getHierarchy());
			ProcessJudgement pjdgt2 = new ProcessJudgement(
					p2, ctxLabel, rho, site, gamma, getHierarchy());
			result = (pjdgt1.check() && pjdgt2.check());
			
		} else if (process instanceof ActsFor) {
			
			result = true;
			
			for (Term t1 : RhoEval.eval(((ActsFor) process).getT1(), rho)) {
				for (Term t2 : RhoEval.eval(((ActsFor) process).getT2(), rho)) {
					
					PrincipalHierarchy phNew = getHierarchy().deepCopy();
					Principal p1 = (Principal) t1;
					Principal p2 = (Principal) t2;
					phNew.addActsFor(p1, p2);
					ProcessJudgement pjdgt1 = new ProcessJudgement(
							((ActsFor) process).getProcess1(),
							ctxLabel, rho, site, gamma, phNew);
					if (!pjdgt1.check()) {
						result = false;
					}
				}
			}
			
			if (result == true) {
				ProcessJudgement pjdgt2 = new ProcessJudgement(
						((ActsFor) process).getProcess2(),
						ctxLabel, rho, site, gamma, getHierarchy());
				if (!pjdgt2.check()) {
					result = false;
				}
			}
			
		} else if (process instanceof Go) {
			
			result = true; 
			
			for (Term tc : RhoEval.eval(((Go) process).getTerm(), rho)) {
				Site st = (Site) tc;
				ProcessJudgement pjdgt = new ProcessJudgement(
						((Go) process).getProcess(),
						ctxLabel, rho, st, gamma, getHierarchy());
				if (!pjdgt.check()) {
					result = false;
				}
			}
			
		} else {
			assert false;
		}
		 
		return result;
	}
	
	private boolean wfif(Binder binder) throws FunctionUndefinedException
	{
		return wfif1(binder) && wfif2(binder);
	}
	
	private static int counter = 0;
	
	private boolean wfif1(Binder binder) throws FunctionUndefinedException 
	{
		boolean result = false;
		
		if (binder instanceof BasicBinder) {
			result = true;
			return result;
		}
		
		counter = 0;
		ArrayList<Binder> glbList = new ArrayList<Binder>();
		HashMap<Binder, Integer> glbMap = new HashMap<Binder, Integer>(); 
		buildGlbOrdering(binder, glbList, glbMap);
		QualityPredicate glbPred = makeGlobalPredicate(binder, glbMap);
		int numOfBBs = glbList.size();
		byte[] subsetIndices = new byte[numOfBBs];
		HashMap<Integer, ArrayList<TreeSet<Integer>>> bBMap = 
				new HashMap<Integer, ArrayList<TreeSet<Integer>>>();
		for (int i = 0; i < numOfBBs; i++) {
			bBMap.put(new Integer(i), new ArrayList<TreeSet<Integer>>());
		}
		boolean full = false;
		// iterate over all B
		do {
			
			TreeSet<Integer> BInt = new TreeSet<Integer>();
			for (int j = 0; j < numOfBBs; j++) {
				if (subsetIndices[j] == 1) {
					BInt.add(j);
				}
			}
			
			if (BInt.isEmpty()) {
				subsetIndices[0] = 1;
				continue;
			}
			
			// iterate over all the basic binder bk 
			for (int i = 0; i < numOfBBs; i++) {
				if (subsetIndices[i] == 1) { // bk is in B
					continue;
				} else {
					
					boolean tooBig = false;
					for (TreeSet<Integer> ts : bBMap.get(i)) {
						if (BInt.containsAll(ts)) {
							tooBig = true;
							break;
						}
					}
					if (tooBig)
						continue;
					
					// B \ssearrow bk (i) ?
					
					boolean[] valuations = new boolean[numOfBBs];
					boolean end = false;
					do {
						boolean[] uVec = Arrays.copyOf(valuations, numOfBBs);
						if (uVec[i] == false) {
							boolean[] vVec = new boolean[numOfBBs];
							for (int l = 0; l < numOfBBs; l++) {
								if (subsetIndices[l] == 0) {
									vVec[l] = uVec[l];
								} else {
									vVec[l] = !uVec[l];
								}
							}
							if (evalFormula(glbPred, uVec) == false &&
								evalFormula(glbPred, vVec) == true) 
							{// B \ssearrow bk (i) holds
								bBMap.get(i).add(BInt);
								break;
							}
						}
						
						end = true;
						for (int k = 0; k < numOfBBs; k++) {
							if (valuations[k] == false) {
								valuations[k] = true;
								end = false;
								break;
							} else {
								valuations[k] = false;
							}
						}
					} while (!end);
				}
			}
			
			full = true;
			for(int i = 0; i < numOfBBs; i++) {
				if (subsetIndices[i] == 0) {
					subsetIndices[i] = 1;
					full = false;
					break;
				} else {
					subsetIndices[i] = 0;
				}
			}
		} while (!full);
		
		result = true;
		
		for (int k = 0; k < numOfBBs; k++) {
			for (TreeSet<Integer> BInt : bBMap.get(k)) {
				for (int j : BInt) {
					
					Binder bj = glbList.get(j);
					Binder bk = glbList.get(k); 
					
					BinderJudgement bjdgt_j = new BinderJudgement(
							bj, rho, site, gamma, getHierarchy());
					HashSet<Label> lbs = new HashSet<Label>();
					for (Term tc : RhoEval.eval(((BasicBinder) bj).getT(), rho)) {
						lbs.addAll(RhoEval.eval(bjdgt_j.lb(tc), rho));
					}
					ArrayList<Label> lbsAL = new ArrayList<Label>();
					lbsAL.addAll(lbs);
					Label l1 = new LabelDisjunction(lbsAL);
					Label l2 = null;
					HashSet<Label> lbAssert = lbAllAssert(binder, bk, new LinkedList<Label>());
					lbAssert.removeAll(lbAllAssert(binder, bj, new LinkedList<Label>()));
					if (!lbAssert.isEmpty()) {
						ArrayList<Label> ll = new ArrayList<Label>();
						ll.addAll(lbAssert);
						l2 = new LabelDisjunction(ll);
					} else {
						BinderJudgement bjdgt_k = new BinderJudgement(
								bk, rho, site, gamma, getHierarchy());
						HashSet<Label> lbs2 = new HashSet<Label>();
						for (Term tc : RhoEval.eval(((BasicBinder) bk).getT(), rho)) {
							lbs2.addAll(RhoEval.eval(bjdgt_k.lbc(tc), rho));
						}
						ArrayList<Label> lbsAL2 = new ArrayList<Label>();
						lbsAL2.addAll(lbs2);
						l2 = new LabelConjunction(lbsAL2);
					}
					RelabellingJudgement rejdgt = new RelabellingJudgement(
							getHierarchy(), l1, l2);
					if (!rejdgt.check()) {
						result = false;
						return result;
					}
				}
			}
		}
		
		return result;
	}
	
	private HashSet<Label> lbAllAssert(Binder b, Binder bi, LinkedList<Label> stack) 
	{
		HashSet<Label> result = new HashSet<Label>();
		
		if (b instanceof CompositeBinder) {
			ArrayList<Binder> components = ((CompositeBinder) b).getComponentBinders();
			for (Binder bd : components) {
				result = lbAllAssert(bd, bi, stack);
				if (!result.isEmpty())
					return result;
			}
		} else if (b instanceof Assert) {
			stack.push(((Assert) b).getL1());
			result = lbAllAssert(((Assert) b).getBinder(), bi, stack);
			if (!result.isEmpty()) 
				return result;
			stack.pop();
		} else if (b instanceof BasicBinder) {
			if (b.equals(bi)) {
				result.addAll(stack);
				return result;
			}
		}
		
		return result;
	}
	
	private boolean evalFormula(QualityPredicate formula, boolean[] valuations) {
		
		boolean result = false;
		
		// we don't have "forall" and "exits" anymore
		if (formula instanceof AndPredicate) {
			result = true;
			for (QualityPredicate op : ((AndPredicate) formula).getOps()) {
				if (evalFormula(op, valuations) == false) {
					result = false;
					break;
				}
			}
		} else if (formula instanceof OrPredicate) {
			result = false;
			for (QualityPredicate op : ((OrPredicate) formula).getOps()) {
				if (evalFormula(op, valuations) == true) {
					result = true;
					break;
				}
			}
		} else if (formula instanceof NumPredicate) {
			result = valuations[((NumPredicate) formula).getNum()];
		}
		
		return result;
	}
	
	private void buildGlbOrdering(
			Binder binder,
			ArrayList<Binder> glbList, 
			HashMap<Binder, Integer> glbMap)
	{
		if (binder instanceof CompositeBinder) {
			for (Binder bd : ((CompositeBinder) binder).getComponentBinders())
			{
				buildGlbOrdering(bd, glbList, glbMap);
			}
		} else if (binder instanceof Assert) {
			
			buildGlbOrdering(((Assert) binder).getBinder(), glbList, glbMap);
			
		} else if (binder instanceof BasicBinder) {
			
			glbList.add(binder);
			glbMap.put(binder, new Integer(counter));
			counter++;
		}
	}
	
	private QualityPredicate makeGlobalPredicate(
			Binder binder, 
			HashMap<Binder, Integer> glbMap) 
	{
		QualityPredicate result = null;
		
		if (binder instanceof CompositeBinder) {
			
			QualityPredicate pred = ((CompositeBinder) binder).getQ();
			result = doMakeGlobalPredicate(binder, pred, glbMap);
			
		} else if (binder instanceof Assert) {
			
			result = makeGlobalPredicate(((Assert) binder).getBinder(), glbMap);
			
		} else if (binder instanceof BasicBinder) {
			
			result = new NumPredicate(glbMap.get(binder));
		}
		
		return result;
	}
	
	private QualityPredicate doMakeGlobalPredicate(
			Binder binder,
			QualityPredicate predicate,
			HashMap<Binder, Integer> glbMap)
	{
		QualityPredicate result = null;
		
		if (predicate instanceof AndPredicate) {
			
			ArrayList<QualityPredicate> pl = new ArrayList<QualityPredicate>();
			for (QualityPredicate op : ((AndPredicate) predicate).getOps()) {
				pl.add(doMakeGlobalPredicate(binder, op, glbMap));
			}
			result = new AndPredicate(pl);
			
		} else if (predicate instanceof OrPredicate) {
			
			ArrayList<QualityPredicate> pl = new ArrayList<QualityPredicate>();
			for (QualityPredicate op : ((OrPredicate) predicate).getOps()) {
				pl.add(doMakeGlobalPredicate(binder, op, glbMap));
			}
			result = new OrPredicate(pl);
			
		} else if (predicate instanceof ForallPredicate) {
		
			ArrayList<QualityPredicate> pl = new ArrayList<QualityPredicate>();
			for (Binder bb : ((CompositeBinder) binder).getComponentBinders()) {
				pl.add(makeGlobalPredicate(bb, glbMap));
			}
			result = new AndPredicate(pl);
			
		} else if (predicate instanceof ExistsPredicate) {
			
			ArrayList<QualityPredicate> pl = new ArrayList<QualityPredicate>();
			for (Binder bb : ((CompositeBinder) binder).getComponentBinders()) {
				pl.add(makeGlobalPredicate(bb, glbMap));
			}
			result = new OrPredicate(pl);
			
		} else if(predicate instanceof NumPredicate) {
			
			ArrayList<Binder> bbs = ((CompositeBinder) binder).getComponentBinders();
			result = makeGlobalPredicate(
						bbs.get(((NumPredicate) predicate).getNum() - 1),
						glbMap);
		}
		
		return result;
	}
	
	private boolean wfif2(Binder binder) throws FunctionUndefinedException 
	{
		boolean result = true;
		
		counter = 0;
		ArrayList<Binder> glbList = new ArrayList<Binder>();
		HashMap<Binder, Integer> glbMap = new HashMap<Binder, Integer>(); 
		buildGlbOrdering(binder, glbList, glbMap);
		
		for (Binder bd : glbList) {
			Term t = ((BasicBinder) bd).getT();
			HashSet<Term> tcs = RhoEval.eval(t, rho);
			BinderJudgement bdjdgt = new BinderJudgement(bd, rho, site, gamma, getHierarchy());
			for (Term tc : tcs) {
				ArrayList<Label> list1 = new ArrayList<Label>(); 
				list1.addAll(RhoEval.eval(bdjdgt.lb(tc), rho));
				Label l1 = new LabelDisjunction(list1);
				
				ArrayList<Label> list21 = new ArrayList<Label>();
				list21.addAll(RhoEval.eval(bdjdgt.lbc(tc), rho));
				Label l21 = new LabelConjunction(list21);
				HashSet<Label> set22 = lbAllAssert(binder, bd, new LinkedList<Label>());
				ArrayList<Label> list22 = new ArrayList<Label>(); 
				list22.addAll(set22);
				Label l2;
				if (list22.size() > 0) {
					Label l22 = new LabelDisjunction(list22);
					l2 = new LabelDisjunction(l21, l22);
				} else {
					l2 = l21;
				}
				
				RelabellingJudgement rejdgt = new RelabellingJudgement(getHierarchy(), l1, l2);
				if (!rejdgt.check()) {
					result = false;
					return result;
				}
			}
		}
		
		return result;
	}
	
}
